I have intentionally kept this at the level of "single tick" counting of costs. It is a fairly straightforward change to make this more flexible, which I have not done here to ease reviewing of the essential idea of using monad parametricity.

@kim-em : This is duplicating #372 (refinement of #275) is it not? Also there I have a specific meaning of queries which are pre-declared inductive types there. I think the reuse of the word query might cause confusion here.

@sgraf812 : Related question, could we set up mvcgen for the framework in #372 ? Essentially it runs code in Id monad and measures complexity in TimeM (which is just an additive writer monad).

This is duplicating #372 (refinement of #275) is it not?

No, I am proposing that this is a better alternative.

This is duplicating #372 (refinement of #275) is it not?

No, I am proposing that this is a better alternative.

I strongly disagree. You don't state your queries up front in your model. So you can't state reductions, lower bounds etc. all this makes use of explicit queries and custom cost functions. Instead you use a lean function as a parameter. This is a huge limitation in algorithms theory and complexity.

In the model of #372, one can formally state multiple RAM models and even DSLs for Turing machines and circuits from circuit complexity. Therefore we can already define uniform circuit classes in complexity which involves writing programs in two different models with two different cost models (TMs and circuits). The fact that I can write circuits tells me that I can also encode parallel algorithms and the equivalence between circuits and parallel algorithms (there are several standard equivalences between these models). I have kept my pr limited to simple examples to keep it focused (the maintainers explicitly asked this). In fact it can even talk about lower bounds.

In summary : the other PR allows for a comprehensive top down treatment of the multitude of models in algorithms and the relationships between them(one of the standard models like RAM and TM could be sink nodes in this relationship network).

What this PR is doing is equivalent to compressing the process of defining a query and an evaluation function (and a cost function) in my PR, by directly providing the interpreted version as a parameter (cmp). But it is losing a lot in the process. So, you get a slight generalisation from evaluating in Id as #372 does, to evaluating in a parametric monad m and adding mvcgen machinery. While this might be a positive, it could just as easily have been done on top of #372, with all the benefits of that approach. This suggests (per project contribution guidelines), that at the very least this PR should have been:

1. Discussed in Zulip first

However, for any major development, it is strongly recommended to discuss first on Zulip (or via a GitHub issue) so that the scope, dependencies, and placement in the library are aligned.

2. Build on top of the existing PR feat: query complexity model for algorithms theory #372 mentioned above.

New definitions should instantiate existing abstractions whenever appropriate

So, you get a slight generalisation from evaluating in Id as #372 does, to evaluating in a parametric monad m

@Shreyas4991, you are misunderstanding the purpose of this PR, and how we achieve security against cost manipulation via parametricity.

New definitions should instantiate existing abstractions whenever appropriate

#372 doesn't "exist" for the purposes of that suggestion, as it hasn't been merged. I suggest comparison between #376 and #372 stay on Zulip, rather than in the PR discussions.

So, you get a slight generalisation from evaluating in Id as #372 does, to evaluating in a parametric monad m

@Shreyas4991, you are misunderstanding the purpose of this PR, and how we achieve security against cost manipulation via parametricity.

In this instance I am certain I do. I am the domain expert here as far as algorithms is concerned. This is merely short-circuiting my approach and shares the exact same limitation mine does, with write-queries, and with a less than optimal design for the purposes my PR serves. The "generalization" is merely trying to hide the evaluation behind an arbitrary monad instead of a free monad with an uninterpreted query.

New definitions should instantiate existing abstractions whenever appropriate

#372 doesn't "exist" for the purposes of that suggestion, as it hasn't been merged. I suggest comparison between

There is no suggestion in that guidelines that a contributing PRs work can be overriden without discussion if it isn't merged already. It is also a core principle of open source etiquette to discuss an idea first, especially if someone is already working on it before making one's own contribution. This ensures that the work and effort of contributors is not devalued or outright erased. I have adhered to this principle with my PR from the beginning via zulip discussions. This PR has violated it.

Open source guides:

Before doing anything, do a quick check to make sure your idea hasn’t been discussed elsewhere. Skim the project’s README, issues (open and closed), mailing list, and Stack Overflow. You don’t have to spend hours going through everything, but a quick search for a few key terms goes a long way.

@Shreyas4991, you mentioned that "our models have the same security from misuse of return." I don't think that's the case. Here's a fully computable algorithm in the framework of #372 that "sorts in zero queries":

/-- Sorting with zero queries. -/
def freeSort {α : Type} (le : α → α → Prop) [DecidableRel le]
    (l : List α) : Prog (SortOpsInsertHead α) (List α) :=
  .pure (l.insertionSort le)

theorem freeSort_correct {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).eval (sortModel le) = l.insertionSort le := by
  simp [freeSort]

theorem freeSort_free {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).time (sortModel le) = 0 := by
  simp [freeSort]

These theorems together assert that sorting can be done correctly with zero comparisons. The root cause: sortModel le requires [DecidableRel le] to interpret queries, and that same instance gives algorithms direct access to comparisons via pure, bypassing the query mechanism entirely.

In the monad-parametric approach of #376, the comparison is an opaque parameter (α × α → m Bool). The cost theorem insertionSort_runsIn : RunsIn insertionSort (fun xs => xs.length * xs.length) has no DecidableRel, Ord, or BEq in its statement — the algorithm has no way to compare elements except through the provided function, and every such call is counted.

To be clear about the limitations of #376: because Lean has classical logic, a noncomputable algorithm could in principle use Classical.choice to distinguish TickM from other monads and cheat. This means we can't use RunsIn to prove lower bounds (a noncomputable counterexample would always exist). But that's not the goal here — the goal is proving upper bounds for specific algorithms. For computable (monad-polymorphic) algorithms, parametricity holds: they can't observe which monad they're running in, so every comparison genuinely goes through cmp, and the RunsIn bound is valid.

The exploit above is not about classical logic — freeSort is fully computable. The issue is structural: the free monad approach necessarily puts [DecidableRel le] in scope (because the model needs it), and nothing prevents algorithms from using it directly.

@Shreyas4991, you mentioned that "our models have the same security from misuse of return." I don't think that's the case. Here's a fully computable algorithm in the framework of #372 that "sorts in zero queries":

/-- Sorting with zero queries. -/
def freeSort {α : Type} (le : α → α → Prop) [DecidableRel le]
    (l : List α) : Prog (SortOpsInsertHead α) (List α) :=
  .pure (l.insertionSort le)

theorem freeSort_correct {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).eval (sortModel le) = l.insertionSort le := by
  simp [freeSort]

theorem freeSort_free {α : Type} (le : α → α → Prop) [DecidableRel le] (l : List α) :
    (freeSort le l).time (sortModel le) = 0 := by
  simp [freeSort]

These theorems together assert that sorting can be done correctly with zero comparisons. The root cause: sortModel le requires [DecidableRel le] to interpret queries, and that same instance gives algorithms direct access to comparisons via pure, bypassing the query mechanism entirely.

In the monad-parametric approach of #376, the comparison is an opaque parameter (α × α → m Bool). The cost theorem insertionSort_runsIn : RunsIn insertionSort (fun xs => xs.length * xs.length) has no DecidableRel, Ord, or BEq in its statement — the algorithm has no way to compare elements except through the provided function, and every such call is counted.

To be clear about the limitations of #376: because Lean has classical logic, a noncomputable algorithm could in principle use Classical.choice to distinguish TickM from other monads and cheat. This means we can't use RunsIn to prove lower bounds (a noncomputable counterexample would always exist). But that's not the goal here — the goal is proving upper bounds for specific algorithms. For computable (monad-polymorphic) algorithms, parametricity holds: they can't observe which monad they're running in, so every comparison genuinely goes through cmp, and the RunsIn bound is valid.

The exploit above is not about classical logic — freeSort is fully computable. The issue is structural: the free monad approach necessarily puts [DecidableRel le] in scope (because the model needs it), and nothing prevents algorithms from using it directly.

It's not an exploit because you are including an instance that the model explicitly does not require . You can do this in your model as well. Concretely take your decidable LE instance and lift, choose a specific monad with a liftM function and you can also lift "let cmp := liftM fun x y => decide <| LE.le x y) into your monad. I use these instances because I find the trade off between the simplicity of these algorithms and detection of cheating trivial.

You are inserting an extra typeclass instance into my def. I can conversely insert a special monad into yours and erase the parametricity. Neither of these are "exploits"

If providing extra instances is fair game then so is specializing the monad parameter to yours. And to be clear, based on my discussion with type theorists, adding proper foolproof parametric polymorhism to a dependently typed system is an open problem (concretely something like ML style modules). Rocq's module system has been mentioned to me as an example (and they just uncovered a soundness bug there yesterday). So if you solve parametricity in lean, please submit it to POPL.

@kim-em to be clear, a Prog should never have typeclass instances. That's the easiest red flag to catch.

please see the actual linearSearch example. It explicitly avoids giving DecidableEq instances and uses a Bool predicate. We can absolutely make this change for the sorting models as well. Nothing about this example is specific to my model and not yours. It is about the specific choice of type for the cmp operation. Your correctness theorem doesn't prove sorting yet. I found it convenient to use List.Pairwise to prove sortedness. In your PR you don't prove this yet. So this is not even a point that we can meaningfully compare on. If someone wrote a function with le : \a -> \a -> Prop in your model, they will face the exact same issue.

Secondly you made a claim about your goals. They are not my goals. The query model is a model that I am building based on what I know will work for algorithms theory. I am working on something that I can use for algorithms theory. The code verification stuff can be handled by Boole and is not my issue. It's arguably better suited for the problem.

Thirdly this PR is just reinventing WriterT monad transformer

Lastly parametric polymorphism requires that I should not be able to supply an explicit m. In Lean you can always do this. So this is not even "parametric polymorphism". That requires something like ML modules. I should have caught this before. Typeclasses implement ad-hoc polymorphism viz the exact opposite.

@kim-em : Update, I just changed the Prop model to a Bool le model for my sorting query and algorithms in cslib#372 . So no [Decidable le] instances are needed anymore. This has absolutely nothing to do with Free Monads and everything to do with me picking a convenient approach.

But as I have mentioned before, nothing stops someone from writing
def insertionSort ... (le : a -> a -> Prop) [DecidableRel le] in your model either (after all now you need to insert the Prop and DecidableRel version as extra parameters in mine now that I have completely switched all my examples to Bool).

So this "exploit" you have found is equivalently applicable in both models (or more clearly, not), since any monadic DSL will allow pure operations and bad instantiation of monads and other parameters (that's a typeclass vs module system problem). Human reviewing is the only guard. What both models do is substantially reduce the surface area for error.

Also (and this is exactly why I think this PR is misguided from a contribution guidelines standpoint), you could have just made a PR to change my model to a ProgT, which would put my queries behind a monad parameter m, if you felt that my method lacked enough safety.

Concretely, in a proper approach, you would have to make a PR on top of #372 :

1. Write a monad transformer version of TimeM (that's your TickT)
2. Write a monad transformer version of FreeM.
3. generalize Prog to ProgT.
4. change queries and models to evaluate to this monadic type.

Instead your PR lays claim to the idea of query complexity in the title, an idea that I have been promoting since even before the debate formalization, and then squanders the power of my model by losing its explicit inductive query types (while also depriving all of us authors the authorship credit that is due), which I have crafted to handle a huge chunk of algorithms theory literature in a top down fashion.

So this "exploit" you have found is equivalently applicable in both models (or more clearly, not), since any monadic DSL will allow pure operations and bad instantiation of monads and other parameters (that's a typeclass vs module system problem). Human reviewing is the only guard. What both models do is substantially reduce the surface area for error.

You continue to misunderstand this PR. I'd prefer to leave this to reviewers at this point. I appreciate you don't like my implicit criticism of #372 here.

So this "exploit" you have found is equivalently applicable in both models (or more clearly, not), since any monadic DSL will allow pure operations and bad instantiation of monads and other parameters (that's a typeclass vs module system problem). Human reviewing is the only guard. What both models do is substantially reduce the surface area for error.

You continue to misunderstand this PR. I'd prefer to leave this to reviewers at this point. I appreciate you don't like my implicit criticism of #372 here.

I would prefer criticism that was accurate and constructive and that actually improved my PR. Seeing as this was neither, and also making false claims about the problem being inherent to a free monad approach, but so blatantly supplying an instance to a Prog, yes I object. I also object to claims that this PR is better than 372 when 372's objectives are misunderstood.

@kim-em I guided GPT to find two hacks in this "parametricity" approach, with the same level of tricks as the aforementioned "hack" in mine. It took less than 5 minutes to type up the explanation to GPT and have it generate working code while I was simultaneously at a workshop understanding a different proof. I hope this clarifies that I actually understand parametricity better and we can do away these silly accusations that I misunderstand this PR. Especially since they were made when I pointed out how I'd reproduce your hacks in this PR and actually produced them. Parametric polymorphism in lean for algorithms was actually discussed in the lean discord in mid 2024.

Link to Zulip

EDIT: The docstring claims are also too strong. You clearly don't need to use the provided cmp operation 😄

New definitions should instantiate existing abstractions whenever appropriate

#372 doesn't "exist" for the purposes of that suggestion, as it hasn't been merged. I suggest comparison between

There is no suggestion in that guidelines that a contributing PRs work can be overriden without discussion if it isn't merged already. It is also a core principle of open source etiquette to discuss an idea first, especially if someone is already working on it before making one's own contribution. This ensures that the work and effort of contributors is not devalued or outright erased. I have adhered to this principle with my PR from the beginning via zulip discussions. This PR has violated it.

Open source guides:

Before doing anything, do a quick check to make sure your idea hasn’t been discussed elsewhere. Skim the project’s README, issues (open and closed), mailing list, and Stack Overflow. You don’t have to spend hours going through everything, but a quick search for a few key terms goes a long way.

Shreyas, obviously proposing to do something in one way does not give you a veto on attempts to do that thing other ways. Equally obviously, I am aware of your work, you have talked about it extensively. I am not particularly interested in having a long discussion with you about this: words are cheaper for you than they are for me!

Please note that I have broken your parametericity based security claims with two hacks very similar to yours and established my earlier claim that the models are equivalent in security. I have provided the link to the examples.

Not only have I disproved your claim that I misunderstand your pr. I have also established that you misunderstand parametric polymorphism, given

1. Your strong claims in the docstring.

2. Your claimed "hack" against my pr.

3. Your claim that this is hack is somehow inherent to free monads (reality check : it's inherent to any monad).

4. The fact that I produced two hacks of a very similar nature on your pr contradicting your claims so far in the docstring. In fact both hacks use the proposals I already made above which you dismissed as me misunderstanding your PR.

5. I have already switched to a Boolean le predicate, invalidating your currently claimed hack.

You say you value your words more. all I am seeing in this PR is false or no justifications for design decisions and a tonne of code. Code is cheap. Anybody can code. LLMs can code. Design is important. Design >>> code. Hence I talk before making big PRs which is the established OSS etiquette.

I rest my case. I have established that this PR offers no more "security against hacks" than mine. I fully recognize that a lightweight framework will invoke tradeoffs between automated guards and reviewers checking definitions.

I find this discussion increasingly toxic and I am forced to continue this to defend my work against incorrect and also not particularly relevant claims, among other things.

Shreyas, obviously proposing to do something in one way does not give you a veto on attempts to do that thing other ways. Equally obviously, I am aware of your work, you have talked about it extensively. I am not particularly interested in having a long discussion with you about this: words are cheaper for you than they are for me!

This is not about vetoing. This about a lack of prior discussion about an overlapping PR similar to what I did before starting my PR. This is about exploring the possibility of building on top of existing approaches. This is basic OSS etiquette. Code is cheap. Design is expensive. This etiquette is very clear that words (discussions) about new and overlapping contributions are more valuable than just coding up a PR.

This PR is a clear violation of basic OSS etiquette.